Nuprl Lemma : set_leq_antisymmetry
13,42
postcript
pdf
s
:POSet{i},
a
,
b
:|
s
|. (
a
b
)
(
b
a
)
(
a
=
b
)
latex
Up
sets
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
AntiSym(
T
;
x
,
y
.
R
(
x
;
y
))
Lemmas
poset
wf
,
poset
properties
origin
s:POSet{i}, a, b:|s|. (a 
b) 
(b a) (a = b) s:POSet{i}, a, b:|s|. (a b) (b a) (a = b) 
Tx:A. B(x)